Left Termination of the query pattern w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

a :- b.
a :- e.
b :- c.
c :- d.
d :- b.
e :- f.
f :- g.
g :- e.

Queries:

a().

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

A_IN → U21(e_in)
A_IN → E_IN
E_IN → U61(f_in)
E_IN → F_IN
F_IN → U71(g_in)
F_IN → G_IN
G_IN → U81(e_in)
G_IN → E_IN
A_IN → U11(b_in)
A_IN → B_IN
B_IN → U31(c_in)
B_IN → C_IN
C_IN → U41(d_in)
C_IN → D_IN
D_IN → U51(b_in)
D_IN → B_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

A_IN → U21(e_in)
A_IN → E_IN
E_IN → U61(f_in)
E_IN → F_IN
F_IN → U71(g_in)
F_IN → G_IN
G_IN → U81(e_in)
G_IN → E_IN
A_IN → U11(b_in)
A_IN → B_IN
B_IN → U31(c_in)
B_IN → C_IN
C_IN → U41(d_in)
C_IN → D_IN
D_IN → U51(b_in)
D_IN → B_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 10 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

D_IN → B_IN
B_IN → C_IN
C_IN → D_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

D_IN → B_IN
B_IN → C_IN
C_IN → D_IN

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

B_IN → C_IN
D_IN → B_IN
C_IN → D_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

B_IN → C_IN
D_IN → B_IN
C_IN → D_IN

The TRS R consists of the following rules:none


s = C_IN evaluates to t =C_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

C_IN → D_IN
with rule C_IN → D_IN at position [] and matcher [ ]

D_IN → B_IN
with rule D_IN → B_IN at position [] and matcher [ ]

B_IN → C_IN
with rule B_IN → C_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

The TRS R consists of the following rules:none


s = F_IN evaluates to t =F_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

F_IN → G_IN
with rule F_IN → G_IN at position [] and matcher [ ]

G_IN → E_IN
with rule G_IN → E_IN at position [] and matcher [ ]

E_IN → F_IN
with rule E_IN → F_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

A_IN → U21(e_in)
A_IN → E_IN
E_IN → U61(f_in)
E_IN → F_IN
F_IN → U71(g_in)
F_IN → G_IN
G_IN → U81(e_in)
G_IN → E_IN
A_IN → U11(b_in)
A_IN → B_IN
B_IN → U31(c_in)
B_IN → C_IN
C_IN → U41(d_in)
C_IN → D_IN
D_IN → U51(b_in)
D_IN → B_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

A_IN → U21(e_in)
A_IN → E_IN
E_IN → U61(f_in)
E_IN → F_IN
F_IN → U71(g_in)
F_IN → G_IN
G_IN → U81(e_in)
G_IN → E_IN
A_IN → U11(b_in)
A_IN → B_IN
B_IN → U31(c_in)
B_IN → C_IN
C_IN → U41(d_in)
C_IN → D_IN
D_IN → U51(b_in)
D_IN → B_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 10 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

D_IN → B_IN
B_IN → C_IN
C_IN → D_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

D_IN → B_IN
B_IN → C_IN
C_IN → D_IN

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

B_IN → C_IN
D_IN → B_IN
C_IN → D_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

B_IN → C_IN
D_IN → B_IN
C_IN → D_IN

The TRS R consists of the following rules:none


s = C_IN evaluates to t =C_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

C_IN → D_IN
with rule C_IN → D_IN at position [] and matcher [ ]

D_IN → B_IN
with rule D_IN → B_IN at position [] and matcher [ ]

B_IN → C_IN
with rule B_IN → C_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

The TRS R consists of the following rules:

a_in → U2(e_in)
e_in → U6(f_in)
f_in → U7(g_in)
g_in → U8(e_in)
U8(e_out) → g_out
U7(g_out) → f_out
U6(f_out) → e_out
U2(e_out) → a_out
a_in → U1(b_in)
b_in → U3(c_in)
c_in → U4(d_in)
d_in → U5(b_in)
U5(b_out) → d_out
U4(d_out) → c_out
U3(c_out) → b_out
U1(b_out) → a_out

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

E_IN → F_IN
F_IN → G_IN
G_IN → E_IN

The TRS R consists of the following rules:none


s = F_IN evaluates to t =F_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

F_IN → G_IN
with rule F_IN → G_IN at position [] and matcher [ ]

G_IN → E_IN
with rule G_IN → E_IN at position [] and matcher [ ]

E_IN → F_IN
with rule E_IN → F_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.